(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isList(V)) → mark(isNeList(V))
active(isList(nil)) → mark(tt)
active(isList(__(V1, V2))) → mark(and(isList(V1), isList(V2)))
active(isNeList(V)) → mark(isQid(V))
active(isNeList(__(V1, V2))) → mark(and(isList(V1), isNeList(V2)))
active(isNeList(__(V1, V2))) → mark(and(isNeList(V1), isList(V2)))
active(isNePal(V)) → mark(isQid(V))
active(isNePal(__(I, __(P, I)))) → mark(and(isQid(I), isPal(P)))
active(isPal(V)) → mark(isNePal(V))
active(isPal(nil)) → mark(tt)
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)
active(isQid(u)) → mark(tt)
active(__(X1, X2)) → __(active(X1), X2)
active(__(X1, X2)) → __(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
and(mark(X1), X2) → mark(and(X1, X2))
proper(__(X1, X2)) → __(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isList(X)) → isList(proper(X))
proper(isNeList(X)) → isNeList(proper(X))
proper(isQid(X)) → isQid(proper(X))
proper(isNePal(X)) → isNePal(proper(X))
proper(isPal(X)) → isPal(proper(X))
proper(a) → ok(a)
proper(e) → ok(e)
proper(i) → ok(i)
proper(o) → ok(o)
proper(u) → ok(u)
__(ok(X1), ok(X2)) → ok(__(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isList(ok(X)) → ok(isList(X))
isNeList(ok(X)) → ok(isNeList(X))
isQid(ok(X)) → ok(isQid(X))
isNePal(ok(X)) → ok(isNePal(X))
isPal(ok(X)) → ok(isPal(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
Rewrite Strategy: FULL
(1) DecreasingLoopProof (EQUIVALENT transformation)
The following loop(s) give(s) rise to the lower bound Ω(n1):
The rewrite sequence
__(mark(X1), X2) →+ mark(__(X1, X2))
gives rise to a decreasing loop by considering the right hand sides subterm at position [0].
The pumping substitution is [X1 / mark(X1)].
The result substitution is [ ].
(2) BOUNDS(n^1, INF)
(3) RenamingProof (EQUIVALENT transformation)
Renamed function symbols to avoid clashes with predefined symbol.
(4) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isList(V)) → mark(isNeList(V))
active(isList(nil)) → mark(tt)
active(isList(__(V1, V2))) → mark(and(isList(V1), isList(V2)))
active(isNeList(V)) → mark(isQid(V))
active(isNeList(__(V1, V2))) → mark(and(isList(V1), isNeList(V2)))
active(isNeList(__(V1, V2))) → mark(and(isNeList(V1), isList(V2)))
active(isNePal(V)) → mark(isQid(V))
active(isNePal(__(I, __(P, I)))) → mark(and(isQid(I), isPal(P)))
active(isPal(V)) → mark(isNePal(V))
active(isPal(nil)) → mark(tt)
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)
active(isQid(u)) → mark(tt)
active(__(X1, X2)) → __(active(X1), X2)
active(__(X1, X2)) → __(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
and(mark(X1), X2) → mark(and(X1, X2))
proper(__(X1, X2)) → __(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isList(X)) → isList(proper(X))
proper(isNeList(X)) → isNeList(proper(X))
proper(isQid(X)) → isQid(proper(X))
proper(isNePal(X)) → isNePal(proper(X))
proper(isPal(X)) → isPal(proper(X))
proper(a) → ok(a)
proper(e) → ok(e)
proper(i) → ok(i)
proper(o) → ok(o)
proper(u) → ok(u)
__(ok(X1), ok(X2)) → ok(__(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isList(ok(X)) → ok(isList(X))
isNeList(ok(X)) → ok(isNeList(X))
isQid(ok(X)) → ok(isQid(X))
isNePal(ok(X)) → ok(isNePal(X))
isPal(ok(X)) → ok(isPal(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
S is empty.
Rewrite Strategy: FULL
(5) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)
Infered types.
(6) Obligation:
TRS:
Rules:
active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isList(V)) → mark(isNeList(V))
active(isList(nil)) → mark(tt)
active(isList(__(V1, V2))) → mark(and(isList(V1), isList(V2)))
active(isNeList(V)) → mark(isQid(V))
active(isNeList(__(V1, V2))) → mark(and(isList(V1), isNeList(V2)))
active(isNeList(__(V1, V2))) → mark(and(isNeList(V1), isList(V2)))
active(isNePal(V)) → mark(isQid(V))
active(isNePal(__(I, __(P, I)))) → mark(and(isQid(I), isPal(P)))
active(isPal(V)) → mark(isNePal(V))
active(isPal(nil)) → mark(tt)
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)
active(isQid(u)) → mark(tt)
active(__(X1, X2)) → __(active(X1), X2)
active(__(X1, X2)) → __(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
and(mark(X1), X2) → mark(and(X1, X2))
proper(__(X1, X2)) → __(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isList(X)) → isList(proper(X))
proper(isNeList(X)) → isNeList(proper(X))
proper(isQid(X)) → isQid(proper(X))
proper(isNePal(X)) → isNePal(proper(X))
proper(isPal(X)) → isPal(proper(X))
proper(a) → ok(a)
proper(e) → ok(e)
proper(i) → ok(i)
proper(o) → ok(o)
proper(u) → ok(u)
__(ok(X1), ok(X2)) → ok(__(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isList(ok(X)) → ok(isList(X))
isNeList(ok(X)) → ok(isNeList(X))
isQid(ok(X)) → ok(isQid(X))
isNePal(ok(X)) → ok(isNePal(X))
isPal(ok(X)) → ok(isPal(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
Types:
active :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
__ :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
mark :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
nil :: mark:nil:tt:a:e:i:o:u:ok
and :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
tt :: mark:nil:tt:a:e:i:o:u:ok
isList :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
isNeList :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
isQid :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
isNePal :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
isPal :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
a :: mark:nil:tt:a:e:i:o:u:ok
e :: mark:nil:tt:a:e:i:o:u:ok
i :: mark:nil:tt:a:e:i:o:u:ok
o :: mark:nil:tt:a:e:i:o:u:ok
u :: mark:nil:tt:a:e:i:o:u:ok
proper :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
ok :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
top :: mark:nil:tt:a:e:i:o:u:ok → top
hole_mark:nil:tt:a:e:i:o:u:ok1_0 :: mark:nil:tt:a:e:i:o:u:ok
hole_top2_0 :: top
gen_mark:nil:tt:a:e:i:o:u:ok3_0 :: Nat → mark:nil:tt:a:e:i:o:u:ok
(7) OrderProof (LOWER BOUND(ID) transformation)
Heuristically decided to analyse the following defined symbols:
active,
__,
isNeList,
and,
isList,
isQid,
isPal,
isNePal,
proper,
topThey will be analysed ascendingly in the following order:
__ < active
isNeList < active
and < active
isList < active
isQid < active
isPal < active
isNePal < active
active < top
__ < proper
isNeList < proper
and < proper
isList < proper
isQid < proper
isPal < proper
isNePal < proper
proper < top
(8) Obligation:
TRS:
Rules:
active(
__(
__(
X,
Y),
Z)) →
mark(
__(
X,
__(
Y,
Z)))
active(
__(
X,
nil)) →
mark(
X)
active(
__(
nil,
X)) →
mark(
X)
active(
and(
tt,
X)) →
mark(
X)
active(
isList(
V)) →
mark(
isNeList(
V))
active(
isList(
nil)) →
mark(
tt)
active(
isList(
__(
V1,
V2))) →
mark(
and(
isList(
V1),
isList(
V2)))
active(
isNeList(
V)) →
mark(
isQid(
V))
active(
isNeList(
__(
V1,
V2))) →
mark(
and(
isList(
V1),
isNeList(
V2)))
active(
isNeList(
__(
V1,
V2))) →
mark(
and(
isNeList(
V1),
isList(
V2)))
active(
isNePal(
V)) →
mark(
isQid(
V))
active(
isNePal(
__(
I,
__(
P,
I)))) →
mark(
and(
isQid(
I),
isPal(
P)))
active(
isPal(
V)) →
mark(
isNePal(
V))
active(
isPal(
nil)) →
mark(
tt)
active(
isQid(
a)) →
mark(
tt)
active(
isQid(
e)) →
mark(
tt)
active(
isQid(
i)) →
mark(
tt)
active(
isQid(
o)) →
mark(
tt)
active(
isQid(
u)) →
mark(
tt)
active(
__(
X1,
X2)) →
__(
active(
X1),
X2)
active(
__(
X1,
X2)) →
__(
X1,
active(
X2))
active(
and(
X1,
X2)) →
and(
active(
X1),
X2)
__(
mark(
X1),
X2) →
mark(
__(
X1,
X2))
__(
X1,
mark(
X2)) →
mark(
__(
X1,
X2))
and(
mark(
X1),
X2) →
mark(
and(
X1,
X2))
proper(
__(
X1,
X2)) →
__(
proper(
X1),
proper(
X2))
proper(
nil) →
ok(
nil)
proper(
and(
X1,
X2)) →
and(
proper(
X1),
proper(
X2))
proper(
tt) →
ok(
tt)
proper(
isList(
X)) →
isList(
proper(
X))
proper(
isNeList(
X)) →
isNeList(
proper(
X))
proper(
isQid(
X)) →
isQid(
proper(
X))
proper(
isNePal(
X)) →
isNePal(
proper(
X))
proper(
isPal(
X)) →
isPal(
proper(
X))
proper(
a) →
ok(
a)
proper(
e) →
ok(
e)
proper(
i) →
ok(
i)
proper(
o) →
ok(
o)
proper(
u) →
ok(
u)
__(
ok(
X1),
ok(
X2)) →
ok(
__(
X1,
X2))
and(
ok(
X1),
ok(
X2)) →
ok(
and(
X1,
X2))
isList(
ok(
X)) →
ok(
isList(
X))
isNeList(
ok(
X)) →
ok(
isNeList(
X))
isQid(
ok(
X)) →
ok(
isQid(
X))
isNePal(
ok(
X)) →
ok(
isNePal(
X))
isPal(
ok(
X)) →
ok(
isPal(
X))
top(
mark(
X)) →
top(
proper(
X))
top(
ok(
X)) →
top(
active(
X))
Types:
active :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
__ :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
mark :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
nil :: mark:nil:tt:a:e:i:o:u:ok
and :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
tt :: mark:nil:tt:a:e:i:o:u:ok
isList :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
isNeList :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
isQid :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
isNePal :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
isPal :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
a :: mark:nil:tt:a:e:i:o:u:ok
e :: mark:nil:tt:a:e:i:o:u:ok
i :: mark:nil:tt:a:e:i:o:u:ok
o :: mark:nil:tt:a:e:i:o:u:ok
u :: mark:nil:tt:a:e:i:o:u:ok
proper :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
ok :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
top :: mark:nil:tt:a:e:i:o:u:ok → top
hole_mark:nil:tt:a:e:i:o:u:ok1_0 :: mark:nil:tt:a:e:i:o:u:ok
hole_top2_0 :: top
gen_mark:nil:tt:a:e:i:o:u:ok3_0 :: Nat → mark:nil:tt:a:e:i:o:u:ok
Generator Equations:
gen_mark:nil:tt:a:e:i:o:u:ok3_0(0) ⇔ nil
gen_mark:nil:tt:a:e:i:o:u:ok3_0(+(x, 1)) ⇔ mark(gen_mark:nil:tt:a:e:i:o:u:ok3_0(x))
The following defined symbols remain to be analysed:
__, active, isNeList, and, isList, isQid, isPal, isNePal, proper, top
They will be analysed ascendingly in the following order:
__ < active
isNeList < active
and < active
isList < active
isQid < active
isPal < active
isNePal < active
active < top
__ < proper
isNeList < proper
and < proper
isList < proper
isQid < proper
isPal < proper
isNePal < proper
proper < top
(9) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol __.
(10) Obligation:
TRS:
Rules:
active(
__(
__(
X,
Y),
Z)) →
mark(
__(
X,
__(
Y,
Z)))
active(
__(
X,
nil)) →
mark(
X)
active(
__(
nil,
X)) →
mark(
X)
active(
and(
tt,
X)) →
mark(
X)
active(
isList(
V)) →
mark(
isNeList(
V))
active(
isList(
nil)) →
mark(
tt)
active(
isList(
__(
V1,
V2))) →
mark(
and(
isList(
V1),
isList(
V2)))
active(
isNeList(
V)) →
mark(
isQid(
V))
active(
isNeList(
__(
V1,
V2))) →
mark(
and(
isList(
V1),
isNeList(
V2)))
active(
isNeList(
__(
V1,
V2))) →
mark(
and(
isNeList(
V1),
isList(
V2)))
active(
isNePal(
V)) →
mark(
isQid(
V))
active(
isNePal(
__(
I,
__(
P,
I)))) →
mark(
and(
isQid(
I),
isPal(
P)))
active(
isPal(
V)) →
mark(
isNePal(
V))
active(
isPal(
nil)) →
mark(
tt)
active(
isQid(
a)) →
mark(
tt)
active(
isQid(
e)) →
mark(
tt)
active(
isQid(
i)) →
mark(
tt)
active(
isQid(
o)) →
mark(
tt)
active(
isQid(
u)) →
mark(
tt)
active(
__(
X1,
X2)) →
__(
active(
X1),
X2)
active(
__(
X1,
X2)) →
__(
X1,
active(
X2))
active(
and(
X1,
X2)) →
and(
active(
X1),
X2)
__(
mark(
X1),
X2) →
mark(
__(
X1,
X2))
__(
X1,
mark(
X2)) →
mark(
__(
X1,
X2))
and(
mark(
X1),
X2) →
mark(
and(
X1,
X2))
proper(
__(
X1,
X2)) →
__(
proper(
X1),
proper(
X2))
proper(
nil) →
ok(
nil)
proper(
and(
X1,
X2)) →
and(
proper(
X1),
proper(
X2))
proper(
tt) →
ok(
tt)
proper(
isList(
X)) →
isList(
proper(
X))
proper(
isNeList(
X)) →
isNeList(
proper(
X))
proper(
isQid(
X)) →
isQid(
proper(
X))
proper(
isNePal(
X)) →
isNePal(
proper(
X))
proper(
isPal(
X)) →
isPal(
proper(
X))
proper(
a) →
ok(
a)
proper(
e) →
ok(
e)
proper(
i) →
ok(
i)
proper(
o) →
ok(
o)
proper(
u) →
ok(
u)
__(
ok(
X1),
ok(
X2)) →
ok(
__(
X1,
X2))
and(
ok(
X1),
ok(
X2)) →
ok(
and(
X1,
X2))
isList(
ok(
X)) →
ok(
isList(
X))
isNeList(
ok(
X)) →
ok(
isNeList(
X))
isQid(
ok(
X)) →
ok(
isQid(
X))
isNePal(
ok(
X)) →
ok(
isNePal(
X))
isPal(
ok(
X)) →
ok(
isPal(
X))
top(
mark(
X)) →
top(
proper(
X))
top(
ok(
X)) →
top(
active(
X))
Types:
active :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
__ :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
mark :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
nil :: mark:nil:tt:a:e:i:o:u:ok
and :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
tt :: mark:nil:tt:a:e:i:o:u:ok
isList :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
isNeList :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
isQid :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
isNePal :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
isPal :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
a :: mark:nil:tt:a:e:i:o:u:ok
e :: mark:nil:tt:a:e:i:o:u:ok
i :: mark:nil:tt:a:e:i:o:u:ok
o :: mark:nil:tt:a:e:i:o:u:ok
u :: mark:nil:tt:a:e:i:o:u:ok
proper :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
ok :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
top :: mark:nil:tt:a:e:i:o:u:ok → top
hole_mark:nil:tt:a:e:i:o:u:ok1_0 :: mark:nil:tt:a:e:i:o:u:ok
hole_top2_0 :: top
gen_mark:nil:tt:a:e:i:o:u:ok3_0 :: Nat → mark:nil:tt:a:e:i:o:u:ok
Generator Equations:
gen_mark:nil:tt:a:e:i:o:u:ok3_0(0) ⇔ nil
gen_mark:nil:tt:a:e:i:o:u:ok3_0(+(x, 1)) ⇔ mark(gen_mark:nil:tt:a:e:i:o:u:ok3_0(x))
The following defined symbols remain to be analysed:
isNeList, active, and, isList, isQid, isPal, isNePal, proper, top
They will be analysed ascendingly in the following order:
isNeList < active
and < active
isList < active
isQid < active
isPal < active
isNePal < active
active < top
isNeList < proper
and < proper
isList < proper
isQid < proper
isPal < proper
isNePal < proper
proper < top
(11) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol isNeList.
(12) Obligation:
TRS:
Rules:
active(
__(
__(
X,
Y),
Z)) →
mark(
__(
X,
__(
Y,
Z)))
active(
__(
X,
nil)) →
mark(
X)
active(
__(
nil,
X)) →
mark(
X)
active(
and(
tt,
X)) →
mark(
X)
active(
isList(
V)) →
mark(
isNeList(
V))
active(
isList(
nil)) →
mark(
tt)
active(
isList(
__(
V1,
V2))) →
mark(
and(
isList(
V1),
isList(
V2)))
active(
isNeList(
V)) →
mark(
isQid(
V))
active(
isNeList(
__(
V1,
V2))) →
mark(
and(
isList(
V1),
isNeList(
V2)))
active(
isNeList(
__(
V1,
V2))) →
mark(
and(
isNeList(
V1),
isList(
V2)))
active(
isNePal(
V)) →
mark(
isQid(
V))
active(
isNePal(
__(
I,
__(
P,
I)))) →
mark(
and(
isQid(
I),
isPal(
P)))
active(
isPal(
V)) →
mark(
isNePal(
V))
active(
isPal(
nil)) →
mark(
tt)
active(
isQid(
a)) →
mark(
tt)
active(
isQid(
e)) →
mark(
tt)
active(
isQid(
i)) →
mark(
tt)
active(
isQid(
o)) →
mark(
tt)
active(
isQid(
u)) →
mark(
tt)
active(
__(
X1,
X2)) →
__(
active(
X1),
X2)
active(
__(
X1,
X2)) →
__(
X1,
active(
X2))
active(
and(
X1,
X2)) →
and(
active(
X1),
X2)
__(
mark(
X1),
X2) →
mark(
__(
X1,
X2))
__(
X1,
mark(
X2)) →
mark(
__(
X1,
X2))
and(
mark(
X1),
X2) →
mark(
and(
X1,
X2))
proper(
__(
X1,
X2)) →
__(
proper(
X1),
proper(
X2))
proper(
nil) →
ok(
nil)
proper(
and(
X1,
X2)) →
and(
proper(
X1),
proper(
X2))
proper(
tt) →
ok(
tt)
proper(
isList(
X)) →
isList(
proper(
X))
proper(
isNeList(
X)) →
isNeList(
proper(
X))
proper(
isQid(
X)) →
isQid(
proper(
X))
proper(
isNePal(
X)) →
isNePal(
proper(
X))
proper(
isPal(
X)) →
isPal(
proper(
X))
proper(
a) →
ok(
a)
proper(
e) →
ok(
e)
proper(
i) →
ok(
i)
proper(
o) →
ok(
o)
proper(
u) →
ok(
u)
__(
ok(
X1),
ok(
X2)) →
ok(
__(
X1,
X2))
and(
ok(
X1),
ok(
X2)) →
ok(
and(
X1,
X2))
isList(
ok(
X)) →
ok(
isList(
X))
isNeList(
ok(
X)) →
ok(
isNeList(
X))
isQid(
ok(
X)) →
ok(
isQid(
X))
isNePal(
ok(
X)) →
ok(
isNePal(
X))
isPal(
ok(
X)) →
ok(
isPal(
X))
top(
mark(
X)) →
top(
proper(
X))
top(
ok(
X)) →
top(
active(
X))
Types:
active :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
__ :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
mark :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
nil :: mark:nil:tt:a:e:i:o:u:ok
and :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
tt :: mark:nil:tt:a:e:i:o:u:ok
isList :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
isNeList :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
isQid :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
isNePal :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
isPal :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
a :: mark:nil:tt:a:e:i:o:u:ok
e :: mark:nil:tt:a:e:i:o:u:ok
i :: mark:nil:tt:a:e:i:o:u:ok
o :: mark:nil:tt:a:e:i:o:u:ok
u :: mark:nil:tt:a:e:i:o:u:ok
proper :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
ok :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
top :: mark:nil:tt:a:e:i:o:u:ok → top
hole_mark:nil:tt:a:e:i:o:u:ok1_0 :: mark:nil:tt:a:e:i:o:u:ok
hole_top2_0 :: top
gen_mark:nil:tt:a:e:i:o:u:ok3_0 :: Nat → mark:nil:tt:a:e:i:o:u:ok
Generator Equations:
gen_mark:nil:tt:a:e:i:o:u:ok3_0(0) ⇔ nil
gen_mark:nil:tt:a:e:i:o:u:ok3_0(+(x, 1)) ⇔ mark(gen_mark:nil:tt:a:e:i:o:u:ok3_0(x))
The following defined symbols remain to be analysed:
and, active, isList, isQid, isPal, isNePal, proper, top
They will be analysed ascendingly in the following order:
and < active
isList < active
isQid < active
isPal < active
isNePal < active
active < top
and < proper
isList < proper
isQid < proper
isPal < proper
isNePal < proper
proper < top
(13) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol and.
(14) Obligation:
TRS:
Rules:
active(
__(
__(
X,
Y),
Z)) →
mark(
__(
X,
__(
Y,
Z)))
active(
__(
X,
nil)) →
mark(
X)
active(
__(
nil,
X)) →
mark(
X)
active(
and(
tt,
X)) →
mark(
X)
active(
isList(
V)) →
mark(
isNeList(
V))
active(
isList(
nil)) →
mark(
tt)
active(
isList(
__(
V1,
V2))) →
mark(
and(
isList(
V1),
isList(
V2)))
active(
isNeList(
V)) →
mark(
isQid(
V))
active(
isNeList(
__(
V1,
V2))) →
mark(
and(
isList(
V1),
isNeList(
V2)))
active(
isNeList(
__(
V1,
V2))) →
mark(
and(
isNeList(
V1),
isList(
V2)))
active(
isNePal(
V)) →
mark(
isQid(
V))
active(
isNePal(
__(
I,
__(
P,
I)))) →
mark(
and(
isQid(
I),
isPal(
P)))
active(
isPal(
V)) →
mark(
isNePal(
V))
active(
isPal(
nil)) →
mark(
tt)
active(
isQid(
a)) →
mark(
tt)
active(
isQid(
e)) →
mark(
tt)
active(
isQid(
i)) →
mark(
tt)
active(
isQid(
o)) →
mark(
tt)
active(
isQid(
u)) →
mark(
tt)
active(
__(
X1,
X2)) →
__(
active(
X1),
X2)
active(
__(
X1,
X2)) →
__(
X1,
active(
X2))
active(
and(
X1,
X2)) →
and(
active(
X1),
X2)
__(
mark(
X1),
X2) →
mark(
__(
X1,
X2))
__(
X1,
mark(
X2)) →
mark(
__(
X1,
X2))
and(
mark(
X1),
X2) →
mark(
and(
X1,
X2))
proper(
__(
X1,
X2)) →
__(
proper(
X1),
proper(
X2))
proper(
nil) →
ok(
nil)
proper(
and(
X1,
X2)) →
and(
proper(
X1),
proper(
X2))
proper(
tt) →
ok(
tt)
proper(
isList(
X)) →
isList(
proper(
X))
proper(
isNeList(
X)) →
isNeList(
proper(
X))
proper(
isQid(
X)) →
isQid(
proper(
X))
proper(
isNePal(
X)) →
isNePal(
proper(
X))
proper(
isPal(
X)) →
isPal(
proper(
X))
proper(
a) →
ok(
a)
proper(
e) →
ok(
e)
proper(
i) →
ok(
i)
proper(
o) →
ok(
o)
proper(
u) →
ok(
u)
__(
ok(
X1),
ok(
X2)) →
ok(
__(
X1,
X2))
and(
ok(
X1),
ok(
X2)) →
ok(
and(
X1,
X2))
isList(
ok(
X)) →
ok(
isList(
X))
isNeList(
ok(
X)) →
ok(
isNeList(
X))
isQid(
ok(
X)) →
ok(
isQid(
X))
isNePal(
ok(
X)) →
ok(
isNePal(
X))
isPal(
ok(
X)) →
ok(
isPal(
X))
top(
mark(
X)) →
top(
proper(
X))
top(
ok(
X)) →
top(
active(
X))
Types:
active :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
__ :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
mark :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
nil :: mark:nil:tt:a:e:i:o:u:ok
and :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
tt :: mark:nil:tt:a:e:i:o:u:ok
isList :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
isNeList :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
isQid :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
isNePal :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
isPal :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
a :: mark:nil:tt:a:e:i:o:u:ok
e :: mark:nil:tt:a:e:i:o:u:ok
i :: mark:nil:tt:a:e:i:o:u:ok
o :: mark:nil:tt:a:e:i:o:u:ok
u :: mark:nil:tt:a:e:i:o:u:ok
proper :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
ok :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
top :: mark:nil:tt:a:e:i:o:u:ok → top
hole_mark:nil:tt:a:e:i:o:u:ok1_0 :: mark:nil:tt:a:e:i:o:u:ok
hole_top2_0 :: top
gen_mark:nil:tt:a:e:i:o:u:ok3_0 :: Nat → mark:nil:tt:a:e:i:o:u:ok
Generator Equations:
gen_mark:nil:tt:a:e:i:o:u:ok3_0(0) ⇔ nil
gen_mark:nil:tt:a:e:i:o:u:ok3_0(+(x, 1)) ⇔ mark(gen_mark:nil:tt:a:e:i:o:u:ok3_0(x))
The following defined symbols remain to be analysed:
isList, active, isQid, isPal, isNePal, proper, top
They will be analysed ascendingly in the following order:
isList < active
isQid < active
isPal < active
isNePal < active
active < top
isList < proper
isQid < proper
isPal < proper
isNePal < proper
proper < top
(15) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol isList.
(16) Obligation:
TRS:
Rules:
active(
__(
__(
X,
Y),
Z)) →
mark(
__(
X,
__(
Y,
Z)))
active(
__(
X,
nil)) →
mark(
X)
active(
__(
nil,
X)) →
mark(
X)
active(
and(
tt,
X)) →
mark(
X)
active(
isList(
V)) →
mark(
isNeList(
V))
active(
isList(
nil)) →
mark(
tt)
active(
isList(
__(
V1,
V2))) →
mark(
and(
isList(
V1),
isList(
V2)))
active(
isNeList(
V)) →
mark(
isQid(
V))
active(
isNeList(
__(
V1,
V2))) →
mark(
and(
isList(
V1),
isNeList(
V2)))
active(
isNeList(
__(
V1,
V2))) →
mark(
and(
isNeList(
V1),
isList(
V2)))
active(
isNePal(
V)) →
mark(
isQid(
V))
active(
isNePal(
__(
I,
__(
P,
I)))) →
mark(
and(
isQid(
I),
isPal(
P)))
active(
isPal(
V)) →
mark(
isNePal(
V))
active(
isPal(
nil)) →
mark(
tt)
active(
isQid(
a)) →
mark(
tt)
active(
isQid(
e)) →
mark(
tt)
active(
isQid(
i)) →
mark(
tt)
active(
isQid(
o)) →
mark(
tt)
active(
isQid(
u)) →
mark(
tt)
active(
__(
X1,
X2)) →
__(
active(
X1),
X2)
active(
__(
X1,
X2)) →
__(
X1,
active(
X2))
active(
and(
X1,
X2)) →
and(
active(
X1),
X2)
__(
mark(
X1),
X2) →
mark(
__(
X1,
X2))
__(
X1,
mark(
X2)) →
mark(
__(
X1,
X2))
and(
mark(
X1),
X2) →
mark(
and(
X1,
X2))
proper(
__(
X1,
X2)) →
__(
proper(
X1),
proper(
X2))
proper(
nil) →
ok(
nil)
proper(
and(
X1,
X2)) →
and(
proper(
X1),
proper(
X2))
proper(
tt) →
ok(
tt)
proper(
isList(
X)) →
isList(
proper(
X))
proper(
isNeList(
X)) →
isNeList(
proper(
X))
proper(
isQid(
X)) →
isQid(
proper(
X))
proper(
isNePal(
X)) →
isNePal(
proper(
X))
proper(
isPal(
X)) →
isPal(
proper(
X))
proper(
a) →
ok(
a)
proper(
e) →
ok(
e)
proper(
i) →
ok(
i)
proper(
o) →
ok(
o)
proper(
u) →
ok(
u)
__(
ok(
X1),
ok(
X2)) →
ok(
__(
X1,
X2))
and(
ok(
X1),
ok(
X2)) →
ok(
and(
X1,
X2))
isList(
ok(
X)) →
ok(
isList(
X))
isNeList(
ok(
X)) →
ok(
isNeList(
X))
isQid(
ok(
X)) →
ok(
isQid(
X))
isNePal(
ok(
X)) →
ok(
isNePal(
X))
isPal(
ok(
X)) →
ok(
isPal(
X))
top(
mark(
X)) →
top(
proper(
X))
top(
ok(
X)) →
top(
active(
X))
Types:
active :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
__ :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
mark :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
nil :: mark:nil:tt:a:e:i:o:u:ok
and :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
tt :: mark:nil:tt:a:e:i:o:u:ok
isList :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
isNeList :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
isQid :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
isNePal :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
isPal :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
a :: mark:nil:tt:a:e:i:o:u:ok
e :: mark:nil:tt:a:e:i:o:u:ok
i :: mark:nil:tt:a:e:i:o:u:ok
o :: mark:nil:tt:a:e:i:o:u:ok
u :: mark:nil:tt:a:e:i:o:u:ok
proper :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
ok :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
top :: mark:nil:tt:a:e:i:o:u:ok → top
hole_mark:nil:tt:a:e:i:o:u:ok1_0 :: mark:nil:tt:a:e:i:o:u:ok
hole_top2_0 :: top
gen_mark:nil:tt:a:e:i:o:u:ok3_0 :: Nat → mark:nil:tt:a:e:i:o:u:ok
Generator Equations:
gen_mark:nil:tt:a:e:i:o:u:ok3_0(0) ⇔ nil
gen_mark:nil:tt:a:e:i:o:u:ok3_0(+(x, 1)) ⇔ mark(gen_mark:nil:tt:a:e:i:o:u:ok3_0(x))
The following defined symbols remain to be analysed:
isQid, active, isPal, isNePal, proper, top
They will be analysed ascendingly in the following order:
isQid < active
isPal < active
isNePal < active
active < top
isQid < proper
isPal < proper
isNePal < proper
proper < top
(17) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol isQid.
(18) Obligation:
TRS:
Rules:
active(
__(
__(
X,
Y),
Z)) →
mark(
__(
X,
__(
Y,
Z)))
active(
__(
X,
nil)) →
mark(
X)
active(
__(
nil,
X)) →
mark(
X)
active(
and(
tt,
X)) →
mark(
X)
active(
isList(
V)) →
mark(
isNeList(
V))
active(
isList(
nil)) →
mark(
tt)
active(
isList(
__(
V1,
V2))) →
mark(
and(
isList(
V1),
isList(
V2)))
active(
isNeList(
V)) →
mark(
isQid(
V))
active(
isNeList(
__(
V1,
V2))) →
mark(
and(
isList(
V1),
isNeList(
V2)))
active(
isNeList(
__(
V1,
V2))) →
mark(
and(
isNeList(
V1),
isList(
V2)))
active(
isNePal(
V)) →
mark(
isQid(
V))
active(
isNePal(
__(
I,
__(
P,
I)))) →
mark(
and(
isQid(
I),
isPal(
P)))
active(
isPal(
V)) →
mark(
isNePal(
V))
active(
isPal(
nil)) →
mark(
tt)
active(
isQid(
a)) →
mark(
tt)
active(
isQid(
e)) →
mark(
tt)
active(
isQid(
i)) →
mark(
tt)
active(
isQid(
o)) →
mark(
tt)
active(
isQid(
u)) →
mark(
tt)
active(
__(
X1,
X2)) →
__(
active(
X1),
X2)
active(
__(
X1,
X2)) →
__(
X1,
active(
X2))
active(
and(
X1,
X2)) →
and(
active(
X1),
X2)
__(
mark(
X1),
X2) →
mark(
__(
X1,
X2))
__(
X1,
mark(
X2)) →
mark(
__(
X1,
X2))
and(
mark(
X1),
X2) →
mark(
and(
X1,
X2))
proper(
__(
X1,
X2)) →
__(
proper(
X1),
proper(
X2))
proper(
nil) →
ok(
nil)
proper(
and(
X1,
X2)) →
and(
proper(
X1),
proper(
X2))
proper(
tt) →
ok(
tt)
proper(
isList(
X)) →
isList(
proper(
X))
proper(
isNeList(
X)) →
isNeList(
proper(
X))
proper(
isQid(
X)) →
isQid(
proper(
X))
proper(
isNePal(
X)) →
isNePal(
proper(
X))
proper(
isPal(
X)) →
isPal(
proper(
X))
proper(
a) →
ok(
a)
proper(
e) →
ok(
e)
proper(
i) →
ok(
i)
proper(
o) →
ok(
o)
proper(
u) →
ok(
u)
__(
ok(
X1),
ok(
X2)) →
ok(
__(
X1,
X2))
and(
ok(
X1),
ok(
X2)) →
ok(
and(
X1,
X2))
isList(
ok(
X)) →
ok(
isList(
X))
isNeList(
ok(
X)) →
ok(
isNeList(
X))
isQid(
ok(
X)) →
ok(
isQid(
X))
isNePal(
ok(
X)) →
ok(
isNePal(
X))
isPal(
ok(
X)) →
ok(
isPal(
X))
top(
mark(
X)) →
top(
proper(
X))
top(
ok(
X)) →
top(
active(
X))
Types:
active :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
__ :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
mark :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
nil :: mark:nil:tt:a:e:i:o:u:ok
and :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
tt :: mark:nil:tt:a:e:i:o:u:ok
isList :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
isNeList :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
isQid :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
isNePal :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
isPal :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
a :: mark:nil:tt:a:e:i:o:u:ok
e :: mark:nil:tt:a:e:i:o:u:ok
i :: mark:nil:tt:a:e:i:o:u:ok
o :: mark:nil:tt:a:e:i:o:u:ok
u :: mark:nil:tt:a:e:i:o:u:ok
proper :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
ok :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
top :: mark:nil:tt:a:e:i:o:u:ok → top
hole_mark:nil:tt:a:e:i:o:u:ok1_0 :: mark:nil:tt:a:e:i:o:u:ok
hole_top2_0 :: top
gen_mark:nil:tt:a:e:i:o:u:ok3_0 :: Nat → mark:nil:tt:a:e:i:o:u:ok
Generator Equations:
gen_mark:nil:tt:a:e:i:o:u:ok3_0(0) ⇔ nil
gen_mark:nil:tt:a:e:i:o:u:ok3_0(+(x, 1)) ⇔ mark(gen_mark:nil:tt:a:e:i:o:u:ok3_0(x))
The following defined symbols remain to be analysed:
isPal, active, isNePal, proper, top
They will be analysed ascendingly in the following order:
isPal < active
isNePal < active
active < top
isPal < proper
isNePal < proper
proper < top
(19) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol isPal.
(20) Obligation:
TRS:
Rules:
active(
__(
__(
X,
Y),
Z)) →
mark(
__(
X,
__(
Y,
Z)))
active(
__(
X,
nil)) →
mark(
X)
active(
__(
nil,
X)) →
mark(
X)
active(
and(
tt,
X)) →
mark(
X)
active(
isList(
V)) →
mark(
isNeList(
V))
active(
isList(
nil)) →
mark(
tt)
active(
isList(
__(
V1,
V2))) →
mark(
and(
isList(
V1),
isList(
V2)))
active(
isNeList(
V)) →
mark(
isQid(
V))
active(
isNeList(
__(
V1,
V2))) →
mark(
and(
isList(
V1),
isNeList(
V2)))
active(
isNeList(
__(
V1,
V2))) →
mark(
and(
isNeList(
V1),
isList(
V2)))
active(
isNePal(
V)) →
mark(
isQid(
V))
active(
isNePal(
__(
I,
__(
P,
I)))) →
mark(
and(
isQid(
I),
isPal(
P)))
active(
isPal(
V)) →
mark(
isNePal(
V))
active(
isPal(
nil)) →
mark(
tt)
active(
isQid(
a)) →
mark(
tt)
active(
isQid(
e)) →
mark(
tt)
active(
isQid(
i)) →
mark(
tt)
active(
isQid(
o)) →
mark(
tt)
active(
isQid(
u)) →
mark(
tt)
active(
__(
X1,
X2)) →
__(
active(
X1),
X2)
active(
__(
X1,
X2)) →
__(
X1,
active(
X2))
active(
and(
X1,
X2)) →
and(
active(
X1),
X2)
__(
mark(
X1),
X2) →
mark(
__(
X1,
X2))
__(
X1,
mark(
X2)) →
mark(
__(
X1,
X2))
and(
mark(
X1),
X2) →
mark(
and(
X1,
X2))
proper(
__(
X1,
X2)) →
__(
proper(
X1),
proper(
X2))
proper(
nil) →
ok(
nil)
proper(
and(
X1,
X2)) →
and(
proper(
X1),
proper(
X2))
proper(
tt) →
ok(
tt)
proper(
isList(
X)) →
isList(
proper(
X))
proper(
isNeList(
X)) →
isNeList(
proper(
X))
proper(
isQid(
X)) →
isQid(
proper(
X))
proper(
isNePal(
X)) →
isNePal(
proper(
X))
proper(
isPal(
X)) →
isPal(
proper(
X))
proper(
a) →
ok(
a)
proper(
e) →
ok(
e)
proper(
i) →
ok(
i)
proper(
o) →
ok(
o)
proper(
u) →
ok(
u)
__(
ok(
X1),
ok(
X2)) →
ok(
__(
X1,
X2))
and(
ok(
X1),
ok(
X2)) →
ok(
and(
X1,
X2))
isList(
ok(
X)) →
ok(
isList(
X))
isNeList(
ok(
X)) →
ok(
isNeList(
X))
isQid(
ok(
X)) →
ok(
isQid(
X))
isNePal(
ok(
X)) →
ok(
isNePal(
X))
isPal(
ok(
X)) →
ok(
isPal(
X))
top(
mark(
X)) →
top(
proper(
X))
top(
ok(
X)) →
top(
active(
X))
Types:
active :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
__ :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
mark :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
nil :: mark:nil:tt:a:e:i:o:u:ok
and :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
tt :: mark:nil:tt:a:e:i:o:u:ok
isList :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
isNeList :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
isQid :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
isNePal :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
isPal :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
a :: mark:nil:tt:a:e:i:o:u:ok
e :: mark:nil:tt:a:e:i:o:u:ok
i :: mark:nil:tt:a:e:i:o:u:ok
o :: mark:nil:tt:a:e:i:o:u:ok
u :: mark:nil:tt:a:e:i:o:u:ok
proper :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
ok :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
top :: mark:nil:tt:a:e:i:o:u:ok → top
hole_mark:nil:tt:a:e:i:o:u:ok1_0 :: mark:nil:tt:a:e:i:o:u:ok
hole_top2_0 :: top
gen_mark:nil:tt:a:e:i:o:u:ok3_0 :: Nat → mark:nil:tt:a:e:i:o:u:ok
Generator Equations:
gen_mark:nil:tt:a:e:i:o:u:ok3_0(0) ⇔ nil
gen_mark:nil:tt:a:e:i:o:u:ok3_0(+(x, 1)) ⇔ mark(gen_mark:nil:tt:a:e:i:o:u:ok3_0(x))
The following defined symbols remain to be analysed:
isNePal, active, proper, top
They will be analysed ascendingly in the following order:
isNePal < active
active < top
isNePal < proper
proper < top
(21) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol isNePal.
(22) Obligation:
TRS:
Rules:
active(
__(
__(
X,
Y),
Z)) →
mark(
__(
X,
__(
Y,
Z)))
active(
__(
X,
nil)) →
mark(
X)
active(
__(
nil,
X)) →
mark(
X)
active(
and(
tt,
X)) →
mark(
X)
active(
isList(
V)) →
mark(
isNeList(
V))
active(
isList(
nil)) →
mark(
tt)
active(
isList(
__(
V1,
V2))) →
mark(
and(
isList(
V1),
isList(
V2)))
active(
isNeList(
V)) →
mark(
isQid(
V))
active(
isNeList(
__(
V1,
V2))) →
mark(
and(
isList(
V1),
isNeList(
V2)))
active(
isNeList(
__(
V1,
V2))) →
mark(
and(
isNeList(
V1),
isList(
V2)))
active(
isNePal(
V)) →
mark(
isQid(
V))
active(
isNePal(
__(
I,
__(
P,
I)))) →
mark(
and(
isQid(
I),
isPal(
P)))
active(
isPal(
V)) →
mark(
isNePal(
V))
active(
isPal(
nil)) →
mark(
tt)
active(
isQid(
a)) →
mark(
tt)
active(
isQid(
e)) →
mark(
tt)
active(
isQid(
i)) →
mark(
tt)
active(
isQid(
o)) →
mark(
tt)
active(
isQid(
u)) →
mark(
tt)
active(
__(
X1,
X2)) →
__(
active(
X1),
X2)
active(
__(
X1,
X2)) →
__(
X1,
active(
X2))
active(
and(
X1,
X2)) →
and(
active(
X1),
X2)
__(
mark(
X1),
X2) →
mark(
__(
X1,
X2))
__(
X1,
mark(
X2)) →
mark(
__(
X1,
X2))
and(
mark(
X1),
X2) →
mark(
and(
X1,
X2))
proper(
__(
X1,
X2)) →
__(
proper(
X1),
proper(
X2))
proper(
nil) →
ok(
nil)
proper(
and(
X1,
X2)) →
and(
proper(
X1),
proper(
X2))
proper(
tt) →
ok(
tt)
proper(
isList(
X)) →
isList(
proper(
X))
proper(
isNeList(
X)) →
isNeList(
proper(
X))
proper(
isQid(
X)) →
isQid(
proper(
X))
proper(
isNePal(
X)) →
isNePal(
proper(
X))
proper(
isPal(
X)) →
isPal(
proper(
X))
proper(
a) →
ok(
a)
proper(
e) →
ok(
e)
proper(
i) →
ok(
i)
proper(
o) →
ok(
o)
proper(
u) →
ok(
u)
__(
ok(
X1),
ok(
X2)) →
ok(
__(
X1,
X2))
and(
ok(
X1),
ok(
X2)) →
ok(
and(
X1,
X2))
isList(
ok(
X)) →
ok(
isList(
X))
isNeList(
ok(
X)) →
ok(
isNeList(
X))
isQid(
ok(
X)) →
ok(
isQid(
X))
isNePal(
ok(
X)) →
ok(
isNePal(
X))
isPal(
ok(
X)) →
ok(
isPal(
X))
top(
mark(
X)) →
top(
proper(
X))
top(
ok(
X)) →
top(
active(
X))
Types:
active :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
__ :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
mark :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
nil :: mark:nil:tt:a:e:i:o:u:ok
and :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
tt :: mark:nil:tt:a:e:i:o:u:ok
isList :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
isNeList :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
isQid :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
isNePal :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
isPal :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
a :: mark:nil:tt:a:e:i:o:u:ok
e :: mark:nil:tt:a:e:i:o:u:ok
i :: mark:nil:tt:a:e:i:o:u:ok
o :: mark:nil:tt:a:e:i:o:u:ok
u :: mark:nil:tt:a:e:i:o:u:ok
proper :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
ok :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
top :: mark:nil:tt:a:e:i:o:u:ok → top
hole_mark:nil:tt:a:e:i:o:u:ok1_0 :: mark:nil:tt:a:e:i:o:u:ok
hole_top2_0 :: top
gen_mark:nil:tt:a:e:i:o:u:ok3_0 :: Nat → mark:nil:tt:a:e:i:o:u:ok
Generator Equations:
gen_mark:nil:tt:a:e:i:o:u:ok3_0(0) ⇔ nil
gen_mark:nil:tt:a:e:i:o:u:ok3_0(+(x, 1)) ⇔ mark(gen_mark:nil:tt:a:e:i:o:u:ok3_0(x))
The following defined symbols remain to be analysed:
active, proper, top
They will be analysed ascendingly in the following order:
active < top
proper < top
(23) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol active.
(24) Obligation:
TRS:
Rules:
active(
__(
__(
X,
Y),
Z)) →
mark(
__(
X,
__(
Y,
Z)))
active(
__(
X,
nil)) →
mark(
X)
active(
__(
nil,
X)) →
mark(
X)
active(
and(
tt,
X)) →
mark(
X)
active(
isList(
V)) →
mark(
isNeList(
V))
active(
isList(
nil)) →
mark(
tt)
active(
isList(
__(
V1,
V2))) →
mark(
and(
isList(
V1),
isList(
V2)))
active(
isNeList(
V)) →
mark(
isQid(
V))
active(
isNeList(
__(
V1,
V2))) →
mark(
and(
isList(
V1),
isNeList(
V2)))
active(
isNeList(
__(
V1,
V2))) →
mark(
and(
isNeList(
V1),
isList(
V2)))
active(
isNePal(
V)) →
mark(
isQid(
V))
active(
isNePal(
__(
I,
__(
P,
I)))) →
mark(
and(
isQid(
I),
isPal(
P)))
active(
isPal(
V)) →
mark(
isNePal(
V))
active(
isPal(
nil)) →
mark(
tt)
active(
isQid(
a)) →
mark(
tt)
active(
isQid(
e)) →
mark(
tt)
active(
isQid(
i)) →
mark(
tt)
active(
isQid(
o)) →
mark(
tt)
active(
isQid(
u)) →
mark(
tt)
active(
__(
X1,
X2)) →
__(
active(
X1),
X2)
active(
__(
X1,
X2)) →
__(
X1,
active(
X2))
active(
and(
X1,
X2)) →
and(
active(
X1),
X2)
__(
mark(
X1),
X2) →
mark(
__(
X1,
X2))
__(
X1,
mark(
X2)) →
mark(
__(
X1,
X2))
and(
mark(
X1),
X2) →
mark(
and(
X1,
X2))
proper(
__(
X1,
X2)) →
__(
proper(
X1),
proper(
X2))
proper(
nil) →
ok(
nil)
proper(
and(
X1,
X2)) →
and(
proper(
X1),
proper(
X2))
proper(
tt) →
ok(
tt)
proper(
isList(
X)) →
isList(
proper(
X))
proper(
isNeList(
X)) →
isNeList(
proper(
X))
proper(
isQid(
X)) →
isQid(
proper(
X))
proper(
isNePal(
X)) →
isNePal(
proper(
X))
proper(
isPal(
X)) →
isPal(
proper(
X))
proper(
a) →
ok(
a)
proper(
e) →
ok(
e)
proper(
i) →
ok(
i)
proper(
o) →
ok(
o)
proper(
u) →
ok(
u)
__(
ok(
X1),
ok(
X2)) →
ok(
__(
X1,
X2))
and(
ok(
X1),
ok(
X2)) →
ok(
and(
X1,
X2))
isList(
ok(
X)) →
ok(
isList(
X))
isNeList(
ok(
X)) →
ok(
isNeList(
X))
isQid(
ok(
X)) →
ok(
isQid(
X))
isNePal(
ok(
X)) →
ok(
isNePal(
X))
isPal(
ok(
X)) →
ok(
isPal(
X))
top(
mark(
X)) →
top(
proper(
X))
top(
ok(
X)) →
top(
active(
X))
Types:
active :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
__ :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
mark :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
nil :: mark:nil:tt:a:e:i:o:u:ok
and :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
tt :: mark:nil:tt:a:e:i:o:u:ok
isList :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
isNeList :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
isQid :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
isNePal :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
isPal :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
a :: mark:nil:tt:a:e:i:o:u:ok
e :: mark:nil:tt:a:e:i:o:u:ok
i :: mark:nil:tt:a:e:i:o:u:ok
o :: mark:nil:tt:a:e:i:o:u:ok
u :: mark:nil:tt:a:e:i:o:u:ok
proper :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
ok :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
top :: mark:nil:tt:a:e:i:o:u:ok → top
hole_mark:nil:tt:a:e:i:o:u:ok1_0 :: mark:nil:tt:a:e:i:o:u:ok
hole_top2_0 :: top
gen_mark:nil:tt:a:e:i:o:u:ok3_0 :: Nat → mark:nil:tt:a:e:i:o:u:ok
Generator Equations:
gen_mark:nil:tt:a:e:i:o:u:ok3_0(0) ⇔ nil
gen_mark:nil:tt:a:e:i:o:u:ok3_0(+(x, 1)) ⇔ mark(gen_mark:nil:tt:a:e:i:o:u:ok3_0(x))
The following defined symbols remain to be analysed:
proper, top
They will be analysed ascendingly in the following order:
proper < top
(25) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol proper.
(26) Obligation:
TRS:
Rules:
active(
__(
__(
X,
Y),
Z)) →
mark(
__(
X,
__(
Y,
Z)))
active(
__(
X,
nil)) →
mark(
X)
active(
__(
nil,
X)) →
mark(
X)
active(
and(
tt,
X)) →
mark(
X)
active(
isList(
V)) →
mark(
isNeList(
V))
active(
isList(
nil)) →
mark(
tt)
active(
isList(
__(
V1,
V2))) →
mark(
and(
isList(
V1),
isList(
V2)))
active(
isNeList(
V)) →
mark(
isQid(
V))
active(
isNeList(
__(
V1,
V2))) →
mark(
and(
isList(
V1),
isNeList(
V2)))
active(
isNeList(
__(
V1,
V2))) →
mark(
and(
isNeList(
V1),
isList(
V2)))
active(
isNePal(
V)) →
mark(
isQid(
V))
active(
isNePal(
__(
I,
__(
P,
I)))) →
mark(
and(
isQid(
I),
isPal(
P)))
active(
isPal(
V)) →
mark(
isNePal(
V))
active(
isPal(
nil)) →
mark(
tt)
active(
isQid(
a)) →
mark(
tt)
active(
isQid(
e)) →
mark(
tt)
active(
isQid(
i)) →
mark(
tt)
active(
isQid(
o)) →
mark(
tt)
active(
isQid(
u)) →
mark(
tt)
active(
__(
X1,
X2)) →
__(
active(
X1),
X2)
active(
__(
X1,
X2)) →
__(
X1,
active(
X2))
active(
and(
X1,
X2)) →
and(
active(
X1),
X2)
__(
mark(
X1),
X2) →
mark(
__(
X1,
X2))
__(
X1,
mark(
X2)) →
mark(
__(
X1,
X2))
and(
mark(
X1),
X2) →
mark(
and(
X1,
X2))
proper(
__(
X1,
X2)) →
__(
proper(
X1),
proper(
X2))
proper(
nil) →
ok(
nil)
proper(
and(
X1,
X2)) →
and(
proper(
X1),
proper(
X2))
proper(
tt) →
ok(
tt)
proper(
isList(
X)) →
isList(
proper(
X))
proper(
isNeList(
X)) →
isNeList(
proper(
X))
proper(
isQid(
X)) →
isQid(
proper(
X))
proper(
isNePal(
X)) →
isNePal(
proper(
X))
proper(
isPal(
X)) →
isPal(
proper(
X))
proper(
a) →
ok(
a)
proper(
e) →
ok(
e)
proper(
i) →
ok(
i)
proper(
o) →
ok(
o)
proper(
u) →
ok(
u)
__(
ok(
X1),
ok(
X2)) →
ok(
__(
X1,
X2))
and(
ok(
X1),
ok(
X2)) →
ok(
and(
X1,
X2))
isList(
ok(
X)) →
ok(
isList(
X))
isNeList(
ok(
X)) →
ok(
isNeList(
X))
isQid(
ok(
X)) →
ok(
isQid(
X))
isNePal(
ok(
X)) →
ok(
isNePal(
X))
isPal(
ok(
X)) →
ok(
isPal(
X))
top(
mark(
X)) →
top(
proper(
X))
top(
ok(
X)) →
top(
active(
X))
Types:
active :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
__ :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
mark :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
nil :: mark:nil:tt:a:e:i:o:u:ok
and :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
tt :: mark:nil:tt:a:e:i:o:u:ok
isList :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
isNeList :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
isQid :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
isNePal :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
isPal :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
a :: mark:nil:tt:a:e:i:o:u:ok
e :: mark:nil:tt:a:e:i:o:u:ok
i :: mark:nil:tt:a:e:i:o:u:ok
o :: mark:nil:tt:a:e:i:o:u:ok
u :: mark:nil:tt:a:e:i:o:u:ok
proper :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
ok :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
top :: mark:nil:tt:a:e:i:o:u:ok → top
hole_mark:nil:tt:a:e:i:o:u:ok1_0 :: mark:nil:tt:a:e:i:o:u:ok
hole_top2_0 :: top
gen_mark:nil:tt:a:e:i:o:u:ok3_0 :: Nat → mark:nil:tt:a:e:i:o:u:ok
Generator Equations:
gen_mark:nil:tt:a:e:i:o:u:ok3_0(0) ⇔ nil
gen_mark:nil:tt:a:e:i:o:u:ok3_0(+(x, 1)) ⇔ mark(gen_mark:nil:tt:a:e:i:o:u:ok3_0(x))
The following defined symbols remain to be analysed:
top
(27) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol top.
(28) Obligation:
TRS:
Rules:
active(
__(
__(
X,
Y),
Z)) →
mark(
__(
X,
__(
Y,
Z)))
active(
__(
X,
nil)) →
mark(
X)
active(
__(
nil,
X)) →
mark(
X)
active(
and(
tt,
X)) →
mark(
X)
active(
isList(
V)) →
mark(
isNeList(
V))
active(
isList(
nil)) →
mark(
tt)
active(
isList(
__(
V1,
V2))) →
mark(
and(
isList(
V1),
isList(
V2)))
active(
isNeList(
V)) →
mark(
isQid(
V))
active(
isNeList(
__(
V1,
V2))) →
mark(
and(
isList(
V1),
isNeList(
V2)))
active(
isNeList(
__(
V1,
V2))) →
mark(
and(
isNeList(
V1),
isList(
V2)))
active(
isNePal(
V)) →
mark(
isQid(
V))
active(
isNePal(
__(
I,
__(
P,
I)))) →
mark(
and(
isQid(
I),
isPal(
P)))
active(
isPal(
V)) →
mark(
isNePal(
V))
active(
isPal(
nil)) →
mark(
tt)
active(
isQid(
a)) →
mark(
tt)
active(
isQid(
e)) →
mark(
tt)
active(
isQid(
i)) →
mark(
tt)
active(
isQid(
o)) →
mark(
tt)
active(
isQid(
u)) →
mark(
tt)
active(
__(
X1,
X2)) →
__(
active(
X1),
X2)
active(
__(
X1,
X2)) →
__(
X1,
active(
X2))
active(
and(
X1,
X2)) →
and(
active(
X1),
X2)
__(
mark(
X1),
X2) →
mark(
__(
X1,
X2))
__(
X1,
mark(
X2)) →
mark(
__(
X1,
X2))
and(
mark(
X1),
X2) →
mark(
and(
X1,
X2))
proper(
__(
X1,
X2)) →
__(
proper(
X1),
proper(
X2))
proper(
nil) →
ok(
nil)
proper(
and(
X1,
X2)) →
and(
proper(
X1),
proper(
X2))
proper(
tt) →
ok(
tt)
proper(
isList(
X)) →
isList(
proper(
X))
proper(
isNeList(
X)) →
isNeList(
proper(
X))
proper(
isQid(
X)) →
isQid(
proper(
X))
proper(
isNePal(
X)) →
isNePal(
proper(
X))
proper(
isPal(
X)) →
isPal(
proper(
X))
proper(
a) →
ok(
a)
proper(
e) →
ok(
e)
proper(
i) →
ok(
i)
proper(
o) →
ok(
o)
proper(
u) →
ok(
u)
__(
ok(
X1),
ok(
X2)) →
ok(
__(
X1,
X2))
and(
ok(
X1),
ok(
X2)) →
ok(
and(
X1,
X2))
isList(
ok(
X)) →
ok(
isList(
X))
isNeList(
ok(
X)) →
ok(
isNeList(
X))
isQid(
ok(
X)) →
ok(
isQid(
X))
isNePal(
ok(
X)) →
ok(
isNePal(
X))
isPal(
ok(
X)) →
ok(
isPal(
X))
top(
mark(
X)) →
top(
proper(
X))
top(
ok(
X)) →
top(
active(
X))
Types:
active :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
__ :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
mark :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
nil :: mark:nil:tt:a:e:i:o:u:ok
and :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
tt :: mark:nil:tt:a:e:i:o:u:ok
isList :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
isNeList :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
isQid :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
isNePal :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
isPal :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
a :: mark:nil:tt:a:e:i:o:u:ok
e :: mark:nil:tt:a:e:i:o:u:ok
i :: mark:nil:tt:a:e:i:o:u:ok
o :: mark:nil:tt:a:e:i:o:u:ok
u :: mark:nil:tt:a:e:i:o:u:ok
proper :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
ok :: mark:nil:tt:a:e:i:o:u:ok → mark:nil:tt:a:e:i:o:u:ok
top :: mark:nil:tt:a:e:i:o:u:ok → top
hole_mark:nil:tt:a:e:i:o:u:ok1_0 :: mark:nil:tt:a:e:i:o:u:ok
hole_top2_0 :: top
gen_mark:nil:tt:a:e:i:o:u:ok3_0 :: Nat → mark:nil:tt:a:e:i:o:u:ok
Generator Equations:
gen_mark:nil:tt:a:e:i:o:u:ok3_0(0) ⇔ nil
gen_mark:nil:tt:a:e:i:o:u:ok3_0(+(x, 1)) ⇔ mark(gen_mark:nil:tt:a:e:i:o:u:ok3_0(x))
No more defined symbols left to analyse.